(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 733
Accept states: [734, 735]
Transitions:
733→734[a_1|0]
733→735[c_1|0]
733→733[b_1|0, d_1|0]
733→736[c_1|1]
733→738[c_1|1]
733→739[a_1|1]
733→741[c_1|2]
736→737[c_1|1]
737→734[d_1|1]
738→735[b_1|1]
738→736[b_1|1]
738→738[b_1|1]
738→741[b_1|1]
738→744[a_1|2]
738→747[c_1|3]
739→740[c_1|1]
740→737[d_1|1]
740→742[d_1|1]
740→746[c_1|2]
740→747[d_1|1]
741→742[c_1|2]
742→739[d_1|2]
742→743[c_1|2]
743→740[b_1|2]
744→745[c_1|2]
745→743[d_1|2]
745→748[d_1|2]
745→750[c_1|3]
746→743[b_1|2]
746→748[b_1|2]
747→748[c_1|3]
748→744[d_1|3]
748→749[c_1|3]
749→745[b_1|3]
750→749[b_1|3]